-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

-- Usage:
--
--  Set up the environment
--     setenv LD_LIBRARY_PATH /opt/exp/gnu/lib:$LD_LIBRARY_PATH
--     setenv PATH /home/ggreif/%NoBackup%/Omega1.4.1:$PATH
--
--  Start the omega interpreter by typing
--     omega Thrist.omg
--  and run your commands on the prompt
--

import "LangPrelude.prg" 
  (head,tail,lookup,member,fst,snd,map,Monad,maybeM,id,ioM,Row,HasType,RCons,RNil,Eq,Equal,
  listM)

kind Doe = Wi | So

data DooBiDoo :: Doe ~> Doe ~> *0 where
  ToWi :: DooBiDoo a Wi
  SoToWi :: DooBiDoo So Wi
  WiToWi :: DooBiDoo Wi Wi
  WiToSo :: DooBiDoo Wi So
  SoTo :: DooBiDoo So b
  ToSo :: DooBiDoo a So

data ShuBiDoo :: Doe ~> Doe ~> *0 where
  WiTo :: ShuBiDoo Wi a

--$   @Definition { A @I thrist is a list-like datastructure
--$ with three type indices. It enforces the invariants that
--$ @List { @Item { it can only contain members of the same type with two type indices
--$ and } @Item { that the type indices of consequtive members must match
--$ up in the specific manner that the second type index of the
--$ left member must equal the first type index of the right one. } } }

--{
data Thrist :: forall (l :: *1) . (l ~> l ~> *)  ~> l ~> l ~> * where
  Nil :: Thrist k a a
  Cons :: k c b -> Thrist k b a -> Thrist k c a
 deriving List(l)
--}

--$   @Note { The name thrist is a portmanteau of thread and list
--$ conveying the essence of a list where the members' types are
--$ threaded up. }

{--@
By means of the @Code { deriving List(l) } declaration
we specified that thrists can be entered in @Omega using
special syntax, making it amenable to reading from the
listener, pattern matching and outputting.
@P The following example session demonstrates this:
--@-}

{- Example session:

prompt> #[]l
 #[]l : forall (a:*1) (b:a ~> a ~> *0) (c:a:*1).Thrist b c c
prompt> #[ToWi]l
 #[ToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> #[ToWi,WiToWi]l
 #[ToWi,WiToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> #[ToWi,WiToWi,ToSo]l
 #[ToWi,WiToWi,ToSo]l : forall (a:Doe).Thrist DooBiDoo a So
prompt> #[ToWi,WiToWi,ToSo,SoTo]l
 #[ToWi,WiToWi,ToSo,SoTo]l : forall (a:Doe) (b:Doe).Thrist DooBiDoo a b
prompt> #[ToWi, WiTo]l
 In the expression: Cons WiTo Nil
 the result type: Thrist ShuBiDoo Wi b
 was not what was expected: Thrist DooBiDoo Wi a

-}

##test "different constants: ShubiDoo   !=   DooBiDoo"
 fail0 = #[ToWi, WiTo]l

cat :: Thrist DooBiDoo a b -> String
cat Nil = ""
cat (Cons ToWi r) = "ToWi " ++ cat r
cat (Cons WiToWi r) = "WiToWi " ++ cat r
cat (Cons WiToSo r) = "WiToSo " ++ cat r
cat (Cons SoTo r) = "SoTo " ++ cat r
cat (Cons ToSo r) = "ToSo " ++ cat r


-- Cat thrist
-- See: http://en.wikipedia.org/wiki/Cat_%28programming_language%29

blow :: Nat ~> Row *0 ~> Row *0
{blow Z s} = s
{blow (S n) s} = RCons t {blow n s}

blowLike :: Nat ~> *0 ~> Row *0 ~> Row *0
{blowLike (S arty) (c -> d) s} = RCons c {blowLike arty d s}
{blowLike Z a s} = s

range :: Nat ~> *0 ~> *0
{range (S arty) (c -> d)} = {range arty d}
{range Z a} = a

countArr :: *0 ~> Nat
{countArr Int} = #0
{countArr Bool} = #0
{countArr Char} = #0
{countArr (a, b)} = #0
{countArr [a]} = #0
{countArr (a->b)} = S {countArr b}

data Tractable :: * ~> * where
  IntTractable :: Tractable Int
  BoolTractable :: Tractable Bool
  CharTractable :: Tractable Char
  PairTractable :: Tractable a -> Tractable b -> Tractable (a, b)
  ListTractable :: Tractable a -> Tractable [a]
  ArrTractable :: Tractable a -> Tractable b -> Tractable (a -> b)
  CatTractable :: ShapeTractable a -> ShapeTractable b -> Tractable (Cat a b)

data Primitive
    = Padd
    | Psub
    | Pmul
    | Pdiv
    | Pgt
    | Plt
    | Pgteq
    | Plteq
    | Pneg
    | Peq
    | Pneq
    | Pmin
    | Pmax
    | Pmap -- made up
    | Pord


data Cat :: (Row *0) ~> (Row *0) ~> *0 where
  Push :: Tractable a -> a -> Cat s (RCons a s)
  Prim :: Tractable c -> Primitive -> (a -> c) -> Cat (RCons a {blowLike {countArr c} c s}) (RCons {range {countArr c} c} s)
  Dup :: Cat (RCons t s) (RCons t (RCons t s))
--  Dig :: Pick Row Nat -> Cat (RCons t s) (RCons t (RCons t s))
  Print :: Cat (RCons t s) s
  PopN :: Nat' (S n) -> Cat {blow (S n) s} s
  Swap :: Cat (RCons a (RCons b s)) (RCons b (RCons a s))
-- Perm :: Pick Row Nat -- TODO
  Add :: Cat (RCons Int (RCons Int s)) (RCons Int s)      -- use Prim instead
  Greater :: Cat (RCons Int (RCons Int s)) (RCons Bool s) -- use Prim instead
  Block :: Thrist Cat b c -> Cat a (RCons (Cat b c) a)
  Quote :: Thrist Cat a b -> Cat a b
  Eval :: Cat (RCons (Cat a b) a) b
  If :: Thrist Cat s t ->
        Thrist Cat s t ->
        Cat (RCons Bool s) t


data ShapeTractable :: (Row *0) ~> * where
  Opaque :: ShapeTractable a
  Ontop :: Tractable b -> ShapeTractable a -> ShapeTractable (RCons b a)
 deriving List(st)
  
tc0 = (let a = Opaque in (CatTractable a (Ontop IntTractable a))) :: Tractable (Cat a (RCons Int a))
tc1 = #[Push tc0 (Push IntTractable 42)]l
tc2 = #[Push tc0 (Push IntTractable 42), Eval]l
tc3 = #[Push tc0 (Push IntTractable 42), Eval, Print]l

strTract = ListTractable CharTractable

intPrim = Prim (ArrTractable IntTractable IntTractable)
add = intPrim Padd (+)
sub = intPrim Psub (-)

intPred = Prim (ArrTractable IntTractable BoolTractable)
gt = intPred Pgt (>)
gteq = intPred Pgteq (>=)

pop = PopN #1

te1 = #[Push IntTractable 42, Dup, Greater, If #[pop, Push strTract "hh"]l #[Push IntTractable 42, Add, Print, Push strTract "hh"]l]l
te1a = #[Push IntTractable 42, Dup, gt, If #[pop, Push strTract "hh"]l #[Push IntTractable 42, Add, Print, Push strTract "hh"]l]l

{- This needs more magic:
showThrist :: (t a b -> String) -> Thrist t a b -> String
showThrist f Nil = ""
showThrist f (Cons t r) = f t ++ showThrist f r
-}

cat' :: Thrist Cat a b -> String
cat' Nil = ""
cat' (Cons (Push _ a) r) = "Push " ++ show a ++ "\n" ++ cat' r
cat' (Cons (Prim _ Padd _) r) = "add\n" ++ cat' r
cat' (Cons (Prim _ Psub _) r) = "sub\n" ++ cat' r
cat' (Cons (Prim _ Pgt  _) r) = "gt\n" ++ cat' r
cat' (Cons Dup r) = "Dup\n" ++ cat' r
cat' (Cons Print r) = "Print\n" ++ cat' r
cat' (Cons (PopN n) r) = "PopN " ++ show n ++ "\n" ++ cat' r
cat' (Cons Swap r) = "Swap\n" ++ cat' r
cat' (Cons (If yes no) r) = "If " ++ show yes ++ " ELSE " ++ show no ++ "\n" ++ cat' r

data Stack :: Row *0 ~> *0 where
  Empty :: Stack RNil
  Pu :: a -> Stack s -> Stack (RCons a s)
 deriving List(s)

{-
proveRange :: Tractable d -> Tractable e -> Equal {range {countArr (e -> d)} (e -> d)} {range {countArr d} d}
proveRange IntTractable e = Eq
proveRange BoolTractable e = Eq
proveRange CharTractable e = Eq
proveRange (ListTractable _) e = Eq
proveRange (PairTractable _ _) e = Eq
proveRange (ArrTractable from to) e = Eq
                                      where theorem because = proveRange to
-}

interpretCat :: (forall a . Thrist Cat a a) -> IO (Stack RNil)
interpretCat thr = interpretCat' thr (returnIO Empty)

interpretCat' :: Thrist Cat a b -> IO (Stack a) -> IO (Stack b)

interpretCat' Nil act = act

interpretCat' thr act =
    case thr of
	     (Cons (Push rep a) r) -> do
				      st <- act
				      interpretCat' r (return (Pu a st))
	     (Cons (PopN (S n)) r) -> do
				      Pu _ st <- act
				      interpretCat' r (popMore n st)
	     (Cons Print r) -> do
			       Pu a st <- act
			       new <- putStr (show a)
			       interpretCat' r (return st)
	     (Cons Dup r) -> do
			     Pu a st <- act
  			     interpretCat' r (return (Pu a (Pu a st)))
	     (Cons Swap r) -> do
			      Pu a st <- act
			      let (Pu b st') = st
			      interpretCat' r (return (Pu b (Pu a st')))
	     (Cons (Prim (ArrTractable x y) p f) r) -> do
	                                             Pu a st <- act
				                     interpretCat' (Cons (Prim y p (f a)) r) (return st)
                                                         -- where theorem because = proveRange y x
	     (Cons (Prim IntTractable _ f) r) -> do
	                                       Pu a st <- act
				               interpretCat' r (return (Pu (f a) st))
	     (Cons (Prim BoolTractable _ f) r) -> do
	                                        Pu a st <- act
				                interpretCat' r (return (Pu (f a) st))
	     (Cons (Prim CharTractable _ f) r) -> do
	                                        Pu a st <- act
				                interpretCat' r (return (Pu (f a) st))
	     (Cons (Prim (PairTractable _ _) _ f) r) -> do
	                                              Pu a st <- act
				                      interpretCat' r (return (Pu (f a) st))
	     (Cons (Prim (ListTractable _) _ f) r) -> do
	                                            Pu a st <- act
				                    interpretCat' r (return (Pu (f a) st))
	     (Cons (If yes no) r) -> do
				     Pu cond st <- act
				     let act' = return st
				     interpretCat' r (if cond then interpretCat' yes act' else interpretCat' no act')
	     (Cons (Block thr) r) -> do
	       st <- act
	       interpretCat' r (return (Pu (Quote thr) st))
	     (Cons Eval r) -> do
	       Pu (Quote thr) st <- act
	       let act' = return st
	       interpretCat' r (interpretCat' thr act')
      where monad ioM

popMore :: Nat' n -> Stack {blow n b} -> IO (Stack b)
popMore Z st = return st
    where monad ioM
popMore (S n) st = do
		   let (Pu _ st') = st
		   popMore n st'
    where monad ioM

##test "was not what was expected"
  te2 = interpretCat (Cons (Push 11) te1)

pushI = Push IntTractable
pushB = Push BoolTractable
pushC = Push CharTractable
pushStr = Push (ListTractable CharTractable)

te3 = interpretCat #[pushI 23, pop]l
te4 = interpretCat #[pushI 42, pushI 11, gt, If #[pushB True]l #[pushB False]l, Print]l
te5 = interpretCat #[pushI 42, pushI 32, pushI 1, add, Swap, Print, Print]l
te6 = interpretCat #[pushI 42, pushI 32, pushI 1, add, Swap, Print, Dup, PopN #2]l
te7 = interpretCat #[pushStr "Fun", Push (ArrTractable CharTractable IntTractable) ord, Prim (ArrTractable (ListTractable CharTractable) (ListTractable IntTractable)) Pmap map, Print]l
te8 = interpretCat #[pushC 'Z', Prim IntTractable Pord ord, pushI 2, add, Print]l
te9 = interpretCat #[pushI 42, Block #[Print]l, Eval]l

optimizeCat :: Thrist Cat a b -> Thrist Cat a b
optimizeCat (i@Cons (If yes no) r) = optimizeIf i yes no r
optimizeCat (Cons (p@Push rep a) r) = Cons p (optimizeCat r)
optimizeCat (Cons (p@Swap) r) = Cons p (optimizeCat r)
optimizeCat Nil = Nil

sameTractable :: Tractable a -> Tractable b -> Maybe (Equal a b)
sameTractable IntTractable IntTractable = Just Eq

sameValue :: Tractable a -> a -> a -> Bool
sameValue IntTractable a b = a == b

splitOff :: Thrist Cat a c -> Thrist Cat a c -> exists b . Maybe (Cat a b, Thrist Cat b c, Thrist Cat b c)
splitOff (Cons (p1@Push rep1 a1) r1) (Cons (Push rep2 a2) r2) = case sameTractable rep1 rep2 of
                                                               Just Eq -> Ex (Just (p1, r1, r2))
splitOff (Cons (s@Swap) r1) (Cons Swap r2) =  Ex (Just (s, r1, r2))



optimizeIf :: Thrist Cat (RCons Bool a) b -> Thrist Cat a c -> Thrist Cat a c -> Thrist Cat c b -> Thrist Cat (RCons Bool a) b

optimizeIf all (Cons (Push rep1 a1) t1) (Cons (Push rep2 a2) t2) rest = case sameTractable rep1 rep2 of
                                                                          Just Eq -> if sameValue rep1 a1 a2 then optimizeCat $ Cons (Push rep1 a1) (Cons Swap (Cons (If t1 t2) rest)) else all
                                                                          _ -> all
----optimizeIf all a b rest = case splitOff a b of
----                            Just (Ex (p, t1, t2)) -> 


--optimizeIf all (Cons (Push rep1 a1) t1) (Cons (Push rep2 a2) t2) rest = if eqStr (show a1) (show a2) then optimizeCat $ Cons (Push rep1 a1) (Cons Swap (Cons (If t1 t2) rest)) else all
--           where theorem splitOff

optimizeIf _ Nil Nil rest = Cons pop rest


optimizeIf all _ _ _ = all

to0 = optimizeCat #[If #[pushI 42]l #[pushI 42]l, Print]l
to1 = optimizeCat #[If #[pushI 42]l #[pushI 43]l, Print]l


------------------------------------
-- representing polynomial datatypes
------------------------------------
{- does not work yet
how :: *0 ~> Row *0
{how (t -> u)} = RCons t {how u}
{how Int} = RCons Int RNil
{how Bool} = RCons Bool RNil

last :: *0 ~> Row *0
{last (t -> u)} = {last u}
{last Int} = Int
{last Bool} = Bool



data Sum :: *0 ~> Row *0 ~> *0 where
  Fin :: Sum a RNil
  Case :: t -> Sum a b -> Sum a {how t}
 deriving List(s)

--tp1 :: Sum Bool (Row a)
tp0 = #[False, True]s
tp1 = #[Nothing, Just]s
-}

##test "Mixup in Decs (not reported yet)"
 Weee :: Row *0
 type Weee = RNil



--$ @Section { Crazy uses of Thrists }
--$ For example we can put functions of type
--$ a->b, b->c into a thrist:

--{
funThrist = #[ord, (+) 2, chr]l

runThrist :: Thrist (->) a b -> a -> b
runThrist Nil b = b
runThrist (Cons f r) a = runThrist r (f a)
--}

{-
-- Example session:

prompt> funThrist
 #[<primfun to1>,<fn>,<primfun to1>]l : Thrist (->) Char Char
prompt> runThrist funThrist
 <fn> : Char -> Char
prompt> runThrist funThrist 'x'
 'z' : Char

-}

--$ @Item { An interesting use are @Code { Equal } thrists
--$ as they can express transitivity relationships of
--$ type equality: @Code { Equal a b /\ Equal b c ==> Equal c a }

plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}

plusZ :: Nat' n -> Equal {plus n Z} n
plusZ Z = Eq
plusZ (S n) = Eq -- :: Equal {plus (S n) Z} (S n) -- reduces to Equal (S {plus n Z}) (S n)
  where theorem because = plusZ n -- :: Equal {plus n Z} n


plusS :: Nat' n -> Equal {plus n (S m)} (S {plus n m})
plusS Z = Eq :: Equal {plus Z (S m)} (S {plus Z m}) --> Equal (S m) (S {plus Z m}) --> Equal m {plus Z m} --> Equal m m
plusS (S n) = Eq --::  Equal {plus (S n) (S m)} (S {plus (S n) m})
                   --> Equal (S {plus n (S m)}) (S (S {plus n m}))
                   --% Equal    {plus n (S m)}     (S {plus n m})
    where theorem because = plusS n


plusCommutes :: Nat' n -> Nat' m -> Equal {plus n m} {plus m n}
plusCommutes Z m = Eq --:: Equal {plus Z m} {plus m Z}
                      -->  Equal m {plus m Z}
    where theorem because = plusZ m

plusCommutes (S n) m = Eq --:: Equal {plus (S n) m} {plus m (S n)}
                          -->  Equal (S {plus n m}) {plus m (S n)}
                          --%  Equal (S {plus n m}) (S {plus m n})
                          --%  Equal    {plus n m}     {plus m n}
    where theorem because1 = plusS m, because2 = plusCommutes n m

impliesZero :: Nat' n -> Nat' m -> Equal {plus n m} m -> Equal m Z

{-
##test "current refinement fails because _a != {plus #0 _a}"
 impliesZero Z m Eq = Eq --? Equal {plus Z m} m -> Equal m Z
                        --> Equal m m -> Equal m Z
-}
{-
##test "Annotation not polymorphic enough"
 impliesZero Z (m :: Nat' m')  (Eq :: Equal m' m') = Eq --? Equal {plus Z m} m -> Equal m Z
                        --> Equal m m -> Equal m Z
-}
impliesZero (S n) m Eq = unreachable --? Equal {plus (S n) m} m -> Equal m Z
                                     --> Equal (S {plus n m}) m -> Equal m Z

{-
impliesZero (S n) Z Eq = unreachable --? Equal {plus (S n) Z} Z -> Equal Z Z
                                     --> Equal (S {plus n Z}) Z -> Equal Z Z
                                     --% Equal (S n) Z -> Equal Z Z
--    where theorem plusZ


impliesZero (S n) (S m) Eq = unreachable --? Equal {plus (S n) (S m)} (S m) -> Equal (S m) Z
                                      --> Equal (S {plus n m}) m -> Equal m Z
-}




--$ I am writing this as an equivalent thrist now


{-
hyp1 :: Nat' a -> Nat' (S b) -> Equal a (S b)
hyp1 #1 #1 = Eq
hyp1 (S a) (S b) = Eq
  where theorem because = hyp1 a b
-}

##test "Does not work yet"
 eqThrist = #[Eq :: Equal a (S b)
           , Eq :: Equal (S b) (S c)
           , Eq :: (S c) a
           ]l
